T:Type, l:T List, P:(TProp). list_all(x.P(x);l)  (x:T. (x  l)  P(x)) 

latex

Definitions	t  T, x:A. B(x), x(s), A & B, x:A. B(x), Prop, ||as||, P  Q, False, A, AB, , l[i], True, P  Q, P & Q, P  Q, (x  l), list_all(x.P(x);l), P  Q, x. t(x), {T}
Lemmas	iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, cons member, iff wf, list all wf, l member wf, true wf, nat wf, select wf, length wf2